Cohesive Type Theory
Для любителей монад у меня есть хорошая новость, самое последнее расширение HoTT, cohesivett, или модальная теория типов, которая синтаксически хачит такие штуки как линейность, окресности, связность, бесконечно малые и шейпы как фундаментальные инфинити групоиды. Там три вида контекстов Γ | ∆ | Ξ. И 6 операций — cohesive модалити ʃ (групоид, комонада) ⊣ ♭ (комонада, дискретность) ⊣ ♯ (монада, кодискр.) и дифференциальные модалити ℜ (редукции, комонада, гладкость) ⊣ ℑ (бесконечно малые фиг. модальности, монада) ⊣ & (étale морфизмы, комонада).
Модальная теория типов. Загнали акиомы и погнали. Невозможно же посчитать бесконечно малые. Можно сюда алгоритмы вставить которые будут комонадично считать до определенной точности или в тайпчекер зашить! Тут записано Infinitesimal Shape Modality — коредуцированные объекты.
Im : U -> U
ImUnit (A: U) : A -> Im A
isCoreduced (A:U): U = isEquiv A (Im A) (ImUnit A)
ImCoreduced (A:U): isCoreduced (Im A)
ImRecursion (A B: U) (c: isCoreduced B) (f: A -> B)
: Im A -> B
ImComputeRecursion (A B : U) (c : isCoreduced B) (f : A -> B) (a : A)
: PathP(<i>B)((ImRecursion A B c f)(ImUnit A a))(f a)
ImApp (A B: U) (f: A -> B): Im A -> Im B
ImNaturality (A B: U) (f: A -> B)
: (a: A) -> Path (Im B) ((ImUnit B) (f a)) ((ImApp A B f) (ImUnit A a))
ImInduction (A : U) (B : Im A->U)
(x : (a: Im A) -> isCoreduced(B a))
(y : (a : A) -> B (ImUnit A a))
: (a:Im A)->B a
ImComputeInduction (A:U)(B:Im A->U) (c:(a:Im A)->isCoreduced(B a))
(f : (a : A) -> B (ImUnit A a)) (a:A)
: Path (B (ImUnit A a)) (f a) ((ImInduction A B c f) (ImUnit A a))